ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da).
eclbase?(x)  eclbase-test(x)  State(ds)Valtype(da;eclbase-k(x)) 

latex

Definitions	x:A. B(x), P  Q, b, eclbase?(x), t  T, eclbase-k(x), eclbase-test(x), true, false, if b t else f fi, x. t(x), ecl(ds;da), False, x(s), eclbase(k;test), Prop, eclseq(a;b), ecland(a;b), eclor(a;b), [a]*, a.n, eclthrow(a;n), eclcatch(a;l)
Lemmas	true wf, false wf, assert wf, eclbase? wf, ecl wf, fpf wf, Knd wf, Id wf